SherbyNet - /page/wikibook/entry.mu

Micron Document

`:top

`!ESC/Java`! (and more recently `!ESC/Java2`!), the "Extended Static Checker for Java," is a `F33f`_`[programming tool`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Programming_tool]`_`f that attempts to find common `F33f`_`[run-time errors`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Run-time_error]`_`f in `F33f`_`[Java`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Java_(programming_language)]`_`f programs at `F33f`_`[compile time`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Compile_time]`_`f.`:cite-ref-1[`F5bf`_`[1`#cite-note-1]`_`f] The underlying approach used in ESC/Java is referred to as `F33f`_`[extended static checking`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Extended_static_checking]`_`f, which is a collective name referring to a range of techniques for `F33f`_`[statically checking`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Static_code_analysis]`_`f the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the `F33f`_`[bounds of an array`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Bounds_checking]`_`f. This technique was pioneered in ESC/Java (and its predecessor, ESC/`F33f`_`[Modula-3`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Modula-3]`_`f) and can be thought of as an extended form of `F33f`_`[type checking`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Type_checking]`_`f. Extended static checking usually involves the use of an `F33f`_`[automated theorem prover`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Automated_theorem_proving]`_`f and, in ESC/Java, the Simplify theorem prover was used.

ESC/Java is neither `F33f`_`[sound`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Soundness]`_`f nor `F33f`_`[complete`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Completeness_(logic)]`_`f. This was intentional and aims to reduce the number of errors and/or warnings reported to the programmer, in order to make the tool more useful in practice. However, it does mean that: firstly, there are programs that ESC/Java will erroneously consider to be incorrect (known as `*false-positives`*); secondly, there are incorrect programs it will consider to be correct (known as `*false-negatives`*). Examples in the latter category include errors arising from `F33f`_`[modular arithmetic`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Modular_arithmetic]`_`f and/or `F33f`_`[multithreading`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Thread_(computer_science)]`_`f.

ESC/Java was originally developed at the `F33f`_`[Compaq Systems Research Center`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=DEC_Systems_Research_Center]`_`f (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula-3, ended in 1996. In 2002, SRC released the `F33f`_`[source code`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Source_code]`_`f for ESC/Java and related tools. Recent versions of ESC/Java are based around the `F33f`_`[Java Modeling Language`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Java_Modeling_Language]`_`f (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or `*`F33f`_`[pragmas`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Directive_(programming)]`_`f`*.

The `F33f`_`[University of Nijmegen`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Radboud_University_Nijmegen]`_`f's `*Security of Systems`* group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the `F33f`_`[JML`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Java_Modeling_Language]`_`f specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at `F33f`_`[University College Dublin`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=University_College_Dublin]`_`f, which in 2009 moved to the `F33f`_`[IT University of Copenhagen`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=IT_University_of_Copenhagen]`_`f, and in 2012 to the `F33f`_`[Technical University of Denmark`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Technical_University_of_Denmark]`_`f. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple `F33f`_`[theorem provers`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Automated_theorem_prover]`_`f and integration with `F33f`_`[Eclipse`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Eclipse_(software)]`_`f.

OpenJML, the successor of ESC/Java2, is available for Java 1.8.`:cite-ref-2[`F5bf`_`[2`#cite-note-2]`_`f] The source is available at https://github.com/OpenJML

`:cite-ref-3[`F5bf`_`[3`#cite-note-3]`_`f]

>>Contents

• `F0af`_`[See also`#see-also]`_`f

• `F0af`_`[References`#references]`_`f

• `F0af`_`[External links`#external-links]`_`f

-─

>>See also

• `F33f`_`[Java Modeling Language`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Java_Modeling_Language]`_`f (JML)

>>References

`:cite-note-1`!1.`! `F0af`_`[↑`#cite-ref-1]`_`f `:citerefflanaganleinolillibridgenelson2002`aFlanagan, C.; Leino, K.R.M.; Lillibridge, M.; `F33f`_`[Nelson, G.`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Greg_Nelson_(computer_scientist)]`_`f; `F33f`_`[Saxe, J. B.`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=James_B._Saxe]`_`f; `F33f`_`[Stata, R.`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Raymie_Stata]`_`f (2002). `*Extended static checking for Java`*. `*Proceedings of the Conference on Programming Language Design and Implementation`*. pp. 234–245. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1145/512529.512558. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 1-58113-463-0.

`:cite-note-2`!2.`! `F0af`_`[↑`#cite-ref-2]`_`f "OpenJML download site on sourceforge".

`:cite-note-3`!3.`! `F0af`_`[↑`#cite-ref-3]`_`f "Java Modeling Language (JML) / Code / [r9606] /OpenJML/Trunk/OpenJML".

`!Notes`!

• `:citerefflanagankiniry2001`aFlanagan, C.; Kiniry, K. R. M. (2001). `*Houdini, an Annotation Assistant for ESC/Java`*. `*FME 2001: Formal Methods for Increasing Software Productivity`*. Lecture Notes in Computer Science. Vol. 2021. pp. 500–517. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1007/3-540-45251-6_29. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 3-540-41791-5.

• `:citerefcata-ohuisman2002`aCataño, N.; Huisman, M. (2002). `*Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java`*. `*FME 2002:Formal Methods—Getting IT Right`*. Lecture Notes in Computer Science. Vol. 2391. pp. 272–289. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1007/3-540-45614-7_16. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 3-540-43928-5.

• `:citerefcokkiniry2005`aCok, D. R.; Kiniry, J. R. (2005). `*ESC/Java2: uniting ESC/Java and JML`*. `*Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices`*. Lecture Notes in Computer Science. Vol. 3362. pp. 108–128. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1007/978-3-540-30569-9_6. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 3-540-24287-2.

• `:citerefchalinkiniryleavenspoll2006`aChalin, P.; Kiniry, J. R.; Leavens, G. T.; Poll, E. (2006). `*Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2`*. `*Formal Methods for Components and Objects`*. pp. 342–363. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1007/3-540-45614-7_16. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 3-540-36749-7.

• `:citerefcok2006`aCok, D. R. (2006). `*Specifying java iterators with JML and Esc/Java2`*. `*Proceedings of the 2006 conference on Specification and verification of component-based systems`*. pp. 71–74. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1145/1181195.1181210. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 1-59593-586-X.

• `:citerefchalin2006`aChalin, P. (2006). `*Early detection of JML specification errors using ESC/Java2`*. `*Proceedings of the 2006 conference on Specification and verification of component-based systems`*. pp. 25–32. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1145/1181195.1181201. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 1-59593-586-X.

• `:citerefishikawa2009`aIshikawa, H. (2009). `*An Approach for Refactoring using ESC/Java2: A Simple Case Study`*. `*Proceedings of the 2009 conference on New Trends in Software Methodologies, Tools and Techniques`*. pp. 61–72. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 978-1-60750-049-0.

• `:citerefpoll2009`aPoll, E. (2009). `*Teaching Program Specification and Verification Using JML and ESC/Java2`* (PDF). `*Proceedings of the 2nd International Conference on Teaching Formal Methods`*. Lecture Notes in Computer Science. Vol. 5846. pp. 92–104. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1007/978-3-642-04912-5_7. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 978-3-642-04911-8.

• `:citerefjameschalin2009`aJames, P. R.; Chalin, P. (2009). `*ESC4: a modern caching ESC for Java`*. `*Proceedings of the 8th international workshop on Specification and verification of component-based systems`*. pp. 19–26. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1145/1596486.1596491. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 978-1-60558-680-9.

>>External links

• Java Programming Toolkit Source Release

• Extended Static Checking for Java at the `F33f`_`[Wayback Machine`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Wayback_Machine]`_`f (archived December 8, 2005)

• ESC/Java2 at KindSoftware

• SRC-RR-159 Extended Static Checking. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe

• Extended Static Checking Modula-3 at the `F33f`_`[Wayback Machine`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Wayback_Machine]`_`f (archived February 28, 2001)

• Extended Static Checking Computer Science & Engineering Colloquia. University of Washington. 1999.

`c`F0af`_`[↑ Back to top`#top]`_`f`a